\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $T$:Type, $i$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$).
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ = $y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. vartype($i$;$x$) $\subseteq$r ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ \=$\forall$${\it e'}$@$i$.\+
\\[0ex]($\forall$$e$$<$${\it e'}$. $f$((state when $e$)) = $f$((state when ${\it e'}$)))
\\[0ex]$\vee$ ($\exists$\=$e$:E\+
\\[0ex](($e$ $<$loc ${\it e'}$)
\\[0ex]c$\wedge$ \=(($\neg$($f$((state when $e$)) = $f$((state when ${\it e'}$))))\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex]($e$ $<$loc ${\it e''}$)
\\[0ex]$\Rightarrow$ ${\it e''}$ $\leq$loc ${\it e'}$ 
\\[0ex]$\Rightarrow$ ($f$((state when ${\it e''}$)) = $f$((state when ${\it e'}$)) $\in$ $T$)))))
\-\-\-\-
\end{tabbing}